| Definitions |  x:A. B(x), P   Q, [[R]], Prop, State(ds), DeclaredType(ds;x), {T},   x. t(x), t  T, @i: x:T initially x = v, @i: only L affects x : t, @i: only L sends on (l with tg), @i: with declarations ds:dsda:daeffect of k(v) is x := f s v, x : v, @i (with ds: ds action a:T precondition a(v) is P s v), @i: k affects only members of L, @i: k sends only links in L, @i: only members of L read x, if b t else f fi, x : t initially x = v, Feasible(M), P & Q,  b, f(x)?z, Dec(P), xdom(f). v=f(x) P(x;v), 1of(t), mk-ma, , 2of(t), State(ds), Top, ma-frame-compat(A;B), x dom(f), f(x), M.rframe(A.pre p for a), M.frame(k affects x), M.aframe(k affects x), M.rframe(A.effect f of k on y), M.sframe(k sends <l,tg>), M.bframe(k sends on l), M.rframe(A.sends tfL of k on l), deq-member(eq;x;L), reduce(f;k;as), false, Y, P  Q, M.state, M.da(a), z != f(x) P(a;z), A & B, SQType(T), only members of L affect x :t, only L sends on (l with tg), with declarations ds:dsda:daeffect of k(v) is x := f s v, Valtype(da;k), S  T, S  T, (with ds: ds action a:T precondition a(v) is P s v), k affects only members of L, k sends only on links in L, only members of L read x, R-Feasible(R), x(s), Normal(T), Normal(ds), locl(a), False, P  Q, a = b, @i: A, Dsys |